(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const _14-0 (_ BitVec 14))
(declare-const v7 Bool)
(assert v3)
(assert v2)
(declare-const v8 Bool)
(assert (forall ((q0 (_ BitVec 14)) (q1 (_ BitVec 14))) (not (= (bvsmod _14-0 _14-0) q0 (bvsmod _14-0 _14-0) q0 _14-0))))
(assert (and v1 (= _14-0 _14-0 _14-0 _14-0 _14-0)))
(check-sat)
